Nuprl Definition : R-interface-compat 0,22

R-interface-compat(A;B)
== if Rsends?(B)
== if if Reffect?(A)
== if if let k = Reffect-knd(A) in 
== if if if isrcv(k lnk(k) = Rsends-l(B) Rsends-dt(B)(tag(k))?Void  Reffect-T(A) else True fi
== if i; Rsends?(A)
== if i; let k = Rsends-knd(A) in 
== if i; if isrcv(k lnk(k) = Rsends-l(B) Rsends-dt(B)(tag(k))?Void  Rsends-T(A) else True fi
== if else True fi
== else True fi 
latex



clarification:

R-interface-compat(A;B)
== if Rsends?(B)
== if if Reffect?(A)
== if if let k = Reffect-knd(A) in 
== if if if isrcv(k lnk(k) = Rsends-l(B)
== if if if fpf-cap(Rsends-dt(B);IdDeq;tag(k);Void)  Reffect-T(A)
== if if else True fi
== if i; Rsends?(A)
== if i; let k = Rsends-knd(A) in 
== if i; if isrcv(k lnk(k) = Rsends-l(B) fpf-cap(Rsends-dt(B);IdDeq;tag(k);Void)  Rsends-T(A)
== if i; else True fi
== if else True fi
== else True fi 
latex


DefinitionsReffect?(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), let x = a in b(x), Rsends-knd(x1), if b t else f fi, p  q, isrcv(k), a = b, lnk(k), Rsends-l(x1), f(x)?z, Rsends-dt(x1), IdDeq, tag(k), Void, Rsends-T(x1), True
FDL editor aliasesR-interface-compat

origin